from cheqed.core import tactic
from cheqed.core.sequent import Sequent

# I believe that this is just a nice wrapper on a fragment of the
# lambda calculus, with mapping roughly as follows:
#
# Assumption -> Identity Combinator
# Compound -> Variable
# Rule -> Constant
# Branch -> Combination
#
# Perhaps later this correspondance will allow a clean refactoring.

class Plan(object):
    pass

class Assumption(Plan):
    _id_gen = 0

    @classmethod
    def _get_new_id(cls):
        new_id = Assumption._id_gen
        Assumption._id_gen = Assumption._id_gen + 1
        return new_id
        
    def __init__(self):
        self.id = self._get_new_id()
    
    def __repr__(self):
        return 'assumption()'

    def normalize(self, goal):
        return self
    
    def assumptions(self):
        return [self]
    
    def replace(self, assumption, prover):
        if self.id == assumption.id:
            return prover
        return self

    def subgoals(self, goal):
        return [goal]

class Branch(Plan):
    def __init__(self, first, *branches):
        self.first = first
        self.branches = branches

    def assumptions(self):
        branch_assumptions = []
        for branch in self.branches:
            branch_assumptions.extend(branch.assumptions())
        return branch_assumptions
        
    def replace(self, assumption, prover):
        return Branch(self.first,
                      *[b.replace(assumption, prover) for b in self.branches])
        
    def normalize(self, goal):
        first_subgoals = self.first.subgoals(goal)
        if len(first_subgoals) != len(self.branches):
            raise 'Branch error: number of goals must equal number of branches.'
        normalized_branches = []
        for branch, subgoal in zip(self.branches, first_subgoals):
            normalized_branches.append(branch.normalize(subgoal))
        return Branch(self.first, *normalized_branches)
        
    def subgoals(self, goal):
        first_subgoals = self.first.subgoals(goal)
        if len(first_subgoals) != len(self.branches):
            raise 'Branch error: number of goals must equal number of branches.'
        branch_subgoals = []
        for branch, subgoal in zip(self.branches, first_subgoals):
            branch_subgoals.extend(branch.subgoals(subgoal))
        return branch_subgoals

    def __repr__(self):
        return ('branch(%r, %s)'
                % (self.first,
                   ', '.join([repr(branch) for branch in self.branches])))

class Compound(Plan):
    def __init__(self, func, repr_):
        self.func = func
        self.repr_ = repr_

    def assumptions(self):
        return []
        
    def replace(self, assumption, prover):
        return self
        
    def expand(self, goal):
        return self.func(goal)
    
    def normalize(self, goal):
        subgoal_count = len(self.subgoals(goal))
        if subgoal_count == 0:
            return self
        return Branch(self, *[Assumption() for i in range(subgoal_count)])
        
    def subgoals(self, goal):
        return self.expand(goal).subgoals(goal)

    def __repr__(self):
        return self.repr_
        
class Rule(Plan):
    def __init__(self, func, repr_):
        self.func = func
        self.repr_ = repr_

    def assumptions(self):
        return []

    def replace(self, assumption, prover):
        return self
        
    def normalize(self, goal):
        subgoal_count = len(self.subgoals(goal))
        if subgoal_count == 0:
            return self
        return Branch(self, *[Assumption() for i in range(subgoal_count)])
        
    def subgoals(self, goal):
        return self.func(goal)

    def __repr__(self):
        return self.repr_

